prophecy_r_or_w_ok_exprt lowering: adjust for dynamic/static objects #8629
Conversation
We do not need to create comparisons to dead and/or deallocated when handling a dynamic object (which will never be marked "dead") or a static object (which will neither be marked "dead" nor "deallocated"). This avoids unnecessary branches when the prophecy_r_or_w_ok_exprt can now be simplified to a constant.
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## develop #8629 +/- ##
========================================
Coverage 80.37% 80.37%
========================================
Files 1686 1686
Lines 206872 206896 +24
Branches 73 73
========================================
+ Hits 166265 166288 +23
- Misses 40607 40608 +1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
@tautschnig Will this change play nicely with objects created by #include <stddef.h>
#include <assert.h>
void* allocate_on_stack(size_t size) {
void* ptr = __builtin_alloca(size);
return ptr;
}
void main() {
size_t size;
__CPROVER_assume(0 < size 0 && size <= 1000);
unsigned char* ptr = (unsigned char*)allocate_on_stack(size);
assert(__CPROVER_r_ok(ptr)); // expect FAILURE
} |
|
The simplifier doesn't already do that with the lowered expression? |
No, |
Good call-out - I am now contemplating a very different implementation that will defer these kinds of simplifications to symex. |
We do not need to create comparisons to dead and/or deallocated when handling a dynamic object (which will never be marked "dead") or a static object (which will neither be marked "dead" nor "deallocated"). This avoids unnecessary branches when the prophecy_r_or_w_ok_exprt can now be simplified to a constant.